COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	functions as association lists
C00006 00003	facts about alists
C00012 ENDMK
C⊗;
;functions as association lists
(wipe-out)
(get-proofs appl prf ekl sys)

(proof assoc)

(decl (compalist) (infixname: |∞|) (type: |ground⊗ground→ground|) 
      (syntype: constant) (bindingpower: 930))    
(defax compalist |∀alist1 alist2 xa y.nil ∞ alist2=nil∧
                   ((xa.y).alist1) ∞ alist2=(xa.appalist(y,alist2)).(alist1 ∞ alist2)|)
(label compalistdef)

(decl invalist (type: |GROUND→GROUND|))
(defax invalist |∀alist xa y.invalist nil=nil∧
                             invalist((xa.y).alist)=(y.xa).invalist alist|)
(label invalistdef)

(decl idalistp (type: |GROUND→TRUTHVAL|))
(defax idalistp |∀alist xa y.idalistp(nil)∧
                             (idalistp((xa.y).alist)≡xa=y∧idalistp alist)|)
(label idalistpdef)
;facts about alists
(proof alistfacts)

;check the sorts

(axiom |∀alist alist1.alistp(alist  ∞  alist1)|)
(label compalistsort)(label simpinfo)

(axiom |∀alist.allp(λx.atom x,range(alist))⊃alistp invalist(alist)|)
(label invalistsort)

;facts about composition of functions
;five lemmata 

(axiom |∀alist alist1 x.member(x,dom(alist))⊃
       appalist(x,alist ∞ alist1)=appalist(appalist(x,alist),alist1)|)
(label alist_lemma1)(label app_compalist)

(axiom |∀alist alist1.dom(alist ∞ alist1)=dom(alist)|)
(label alist_lemma2)(label dom_compalist)

(axiom |∀alist x.member(x,dom alist)⊃
                (∃y.member(y,range alist)∧appalist(x,alist)=y)|)
(label alist_lemma3) (label nonempty_range)

(axiom |∀alist z.uniqueness dom(alist)∧member(z,range alist)⊃
        (∃x.member(x,dom alist)∧appalist(x,alist)=z)|) 
(label alist_lemma4) (label nonempty_domain)

(axiom |∀alist alist1 za z.¬member(za,range(alist))⊃
                           alist ∞ ((za.z).alist1)=alist ∞ alist1|)
(label compalist_lemma)

;theorem 1: composition of permutations is a permutation
;PERMUTP(ALIST)∧PERMUTP(ALIST1)∧MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))⊃
;PERMUTP(ALIST ∞ ALIST1)

;the steps in the proof of Theorem 1 are the following 
;lemma range compose

(axiom 
   |∀alist alist1.permutp(alist)∧permutp(alist1)∧
                  mklset(dom(alist))=mklset(dom(alist1))⊃
                  mklset(range(alist ∞ alist1))⊂mklset(range(alist1))|)
(label range_compose)

(axiom 
   |∀alist alist1.permutp(alist)∧permutp(alist1)∧
                  mklset(dom(alist))=mklset(dom(alist1))⊃
                  mklset(range(alist1))⊂mklset(range(alist ∞ alist1))|)
(label range_compose)

;composition is well defined for equivalence classes

(axiom |∀alist alist1 alist2.samemap(alist1,alist2)⊃
                             alist ∞ alist1=alist ∞ alist2|)
(label samamap_right)

(axiom |∀alist1 alist2.samemap(alist1,alist2)⊃
                       samemap(alist1 ∞ alist,alist2 ∞ alist)|)
(label samamap_left)

;facts about the identity function

(axiom |∀alist y.idalistp(alist)∧member(y,dom alist)⊃appalist(y,alist)=y|)
(label idalistp_main)

;theorem 2 (i)
;∀ALIST.FUNCTP(ALIST)∧IDALISTP(ALIST)⊃PERMUTP(ALIST)

;theorem 2 (ii)
;IDALISTP(ALIST1)⊃
;(∀ALIST.MKLSET(RANGE(ALIST))⊂MKLSET(DOM(ALIST1))⊃ALIST ∞ ALIST1=ALIST)

;theorem 2 (iii)
;IDALISTP(ALISTID)∧MKLSET(DOM(ALISTID))=MKLSET(DOM(ALIST))⊃
;SAMEMAP(ALISTID ∞ ALIST,ALIST)

;facts about inversion of functions

(axiom |∀alist.allp(λx.atom x,range(alist))⊃dom(invalist(alist))=range(alist)|)
(label dom_invalist)

(axiom |∀alist.allp(λx.atom x,range(alist))⊃range(invalist(alist))=dom(alist)|)
(label range_invalist)

(axiom |∀alist.mklset(dom(alist))=mklset(range(alist))⊃
               allp(λx.atom x,range(alist))|)
(label atomrange)

;we borrow this from the proof alpig:
(axiom |∀alist.permutp(alist)⊃injectp(alist)|)
(label permutp_injectp)

;theorem 3 (i)
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
;       IDALISTP(ALIST ∞ INVALIST(ALIST))

;theorem 3 (ii)
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
;       IDALISTP(INVALIST(ALIST) ∞ ALIST)

;theorem 3 (iii)
;PERMUTP(ALIST)⊃PERMUTP(INVALIST(ALIST))
(save-proofs assoc)